PRISM

Benchmark
Model:zeroconf-pta v.1 (PTA)
Parameter(s)T = 200
Property:incorrect (prob-reach)
Invocation (specific)
./fix-syntax ./prism -javamaxmem 11g -cuddmaxmem 4g -mtbdd -e 1e-6 -maxiters 1000000 zeroconf-pta.prism zeroconf-pta.props --property incorrect -const T=200
Execution
Walltime:1.428832769393921s
Return code:0
Relative Error:4.418853095795927e-08
Log
PRISM
=====

Version: 4.5.dev
Date: Sun Mar 15 03:30:39 UTC 2020
Hostname: e72bdd194fc5
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -mtbdd -e 1e-6 -maxiters 1000000 zeroconf-pta.prism zeroconf-pta.props --property incorrect -const T=200

Parsing model file "zeroconf-pta.prism"...

Type:        PTA
Modules:     sender environment 
Variables:   s probes ip x e y 

Parsing properties file "zeroconf-pta.props"...

2 properties:
(1) "deadline": Pmax=? [ F<=T s=2&ip=2 ]
(2) "incorrect": Pmax=? [ F s=2&ip=2 ]

---------------------------------------------------------------------

Model checking: "incorrect": Pmax=? [ F s=2&ip=2 ]

Building PTA...

PTA: 2 clocks, 23 locations, 26 transitions
Target (s=2&ip=2) satisfied by 3 locations.

Building initial STPG...

Building forwards reachability graph... 27 states
Graph constructed in 0.018 secs.
Graph: 27 symbolic states (1 initial, 2 target)

Model checking STPG...
STPG model checked in 0.02 secs.
27/27 states converged.
Diff across 1 initial state: 9.068567511510972E-12
Lower/upper bounds for 1 initial state: 0.00130151379208389 - 0.0013015138011524575

Initial STPG: 27 states (1 initial), 38 transitions, 26 choices, 25 choice sets, p1max/avg = 1/0.93, p2max/avg = 2/1.04
Final STPG: 27 states (1 initial), 38 transitions, 26 choices, 25 choice sets, p1max/avg = 1/0.93, p2max/avg = 2/1.04

Terminated after 0 refinements in 0.10 secs.

Abstraction-refinement time breakdown:
* 0.06 secs (64.6%) = Building initial STPG
* 0.00 secs (0.0%) = Rebuilding STPG (0 x avg 0.00 secs)
* 0.02 secs (20.8%) = model checking STPG (1 x avg 0.02 secs) (lb=89.5%) (prob0=25.0%) (pre=60.0%) (iters=112)
* 0.00 secs (0.0%) = refinement (0 x avg 0.00 secs)

Final diff across 1 initial state: 9.068567511510972E-12
Final lower/upper bounds for 1 initial state: 0.00130151379208389 - 0.0013015138011524575

Model checking completed in 0.184 secs.

Result (maximum probability): 0.0013015137966181738


Overall running time: 0.686 seconds.